KILLED



    


Runtime Complexity (full) proof of /tmp/tmpiRWOl4/mucrl1.xml









The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

0 CpxTRS


↳1 DecreasingLoopProof (⇔, 10.1 s)


↳2 BOUNDS(n^1, INF)


↳3 RenamingProof (⇔, 0 ms)


↳4 CpxRelTRS


    ↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)


    ↳6 typed CpxTrs


    ↳7 OrderProof (LOWER BOUND(ID), 0 ms)


    ↳8 typed CpxTrs









(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:

or(T, T) → T

or(F, T) → T

or(T, F) → T

or(F, F) → F

and(T, B) → B

and(B, T) → B

and(F, B) → F

and(B, F) → F

imp(T, B) → B

imp(F, B) → T

not(T) → F

not(F) → T

if(T, B1, B2) → B1

if(F, B1, B2) → B2

eq(T, T) → T

eq(F, F) → T

eq(T, F) → F

eq(F, T) → F

eqt(nil, undefined) → F

eqt(nil, pid(N2)) → F

eqt(nil, int(N2)) → F

eqt(nil, cons(H2, T2)) → F

eqt(nil, tuple(H2, T2)) → F

eqt(nil, tuplenil(H2)) → F

eqt(a, nil) → F

eqt(a, a) → T

eqt(a, excl) → F

eqt(a, false) → F

eqt(a, lock) → F

eqt(a, locker) → F

eqt(a, mcrlrecord) → F

eqt(a, ok) → F

eqt(a, pending) → F

eqt(a, release) → F

eqt(a, request) → F

eqt(a, resource) → F

eqt(a, tag) → F

eqt(a, true) → F

eqt(a, undefined) → F

eqt(a, pid(N2)) → F

eqt(a, int(N2)) → F

eqt(a, cons(H2, T2)) → F

eqt(a, tuple(H2, T2)) → F

eqt(a, tuplenil(H2)) → F

eqt(excl, nil) → F

eqt(excl, a) → F

eqt(excl, excl) → T

eqt(excl, false) → F

eqt(excl, lock) → F

eqt(excl, locker) → F

eqt(excl, mcrlrecord) → F

eqt(excl, ok) → F

eqt(excl, pending) → F

eqt(excl, release) → F

eqt(excl, request) → F

eqt(excl, resource) → F

eqt(excl, tag) → F

eqt(excl, true) → F

eqt(excl, undefined) → F

eqt(excl, pid(N2)) → F

eqt(excl, eqt(false, int(N2))) → F

eqt(false, cons(H2, T2)) → F

eqt(false, tuple(H2, T2)) → F

eqt(false, tuplenil(H2)) → F

eqt(lock, nil) → F

eqt(lock, a) → F

eqt(lock, excl) → F

eqt(lock, false) → F

eqt(lock, lock) → T

eqt(lock, locker) → F

eqt(lock, mcrlrecord) → F

eqt(lock, ok) → F

eqt(lock, pending) → F

eqt(lock, release) → F

eqt(lock, request) → F

eqt(lock, resource) → F

eqt(lock, tag) → F

eqt(lock, true) → F

eqt(lock, undefined) → F

eqt(lock, pid(N2)) → F

eqt(lock, int(N2)) → F

eqt(lock, cons(H2, T2)) → F

eqt(lock, tuple(H2, T2)) → F

eqt(lock, tuplenil(H2)) → F

eqt(locker, nil) → F

eqt(locker, a) → F

eqt(locker, excl) → F

eqt(locker, false) → F

eqt(locker, lock) → F

eqt(locker, locker) → T

eqt(locker, mcrlrecord) → F

eqt(locker, ok) → F

eqt(locker, pending) → F

eqt(locker, release) → F

eqt(locker, request) → F

eqt(locker, resource) → F

eqt(locker, tag) → F

eqt(locker, true) → F

eqt(locker, undefined) → F

eqt(locker, pid(N2)) → F

eqt(locker, int(N2)) → F

eqt(locker, cons(H2, T2)) → F

eqt(locker, tuple(H2, T2)) → F

eqt(locker, tuplenil(H2)) → F

eqt(mcrlrecord, nil) → F

eqt(mcrlrecord, a) → F

eqt(mcrlrecord, excl) → F

eqt(mcrlrecord, false) → F

eqt(mcrlrecord, lock) → F

eqt(mcrlrecord, locker) → F

eqt(mcrlrecord, mcrlrecord) → T

eqt(mcrlrecord, ok) → F

eqt(mcrlrecord, pending) → F

eqt(mcrlrecord, release) → F

eqt(mcrlrecord, request) → F

eqt(mcrlrecord, resource) → F

eqt(ok, resource) → F

eqt(ok, tag) → F

eqt(ok, true) → F

eqt(ok, undefined) → F

eqt(ok, pid(N2)) → F

eqt(ok, int(N2)) → F

eqt(ok, cons(H2, T2)) → F

eqt(ok, tuple(H2, T2)) → F

eqt(ok, tuplenil(H2)) → F

eqt(pending, nil) → F

eqt(pending, a) → F

eqt(pending, excl) → F

eqt(pending, false) → F

eqt(pending, lock) → F

eqt(pending, locker) → F

eqt(pending, mcrlrecord) → F

eqt(pending, ok) → F

eqt(pending, pending) → T

eqt(pending, release) → F

eqt(pending, request) → F

eqt(pending, resource) → F

eqt(pending, tag) → F

eqt(pending, true) → F

eqt(pending, undefined) → F

eqt(pending, pid(N2)) → F

eqt(pending, int(N2)) → F

eqt(pending, cons(H2, T2)) → F

eqt(pending, tuple(H2, T2)) → F

eqt(pending, tuplenil(H2)) → F

eqt(release, nil) → F

eqt(release, a) → F

eqt(release, excl) → F

eqt(release, false) → F

eqt(release, lock) → F

eqt(release, locker) → F

eqt(release, mcrlrecord) → F

eqt(release, ok) → F

eqt(request, mcrlrecord) → F

eqt(request, ok) → F

eqt(request, pending) → F

eqt(request, release) → F

eqt(request, request) → T

eqt(request, resource) → F

eqt(request, tag) → F

eqt(request, true) → F

eqt(request, undefined) → F

eqt(request, pid(N2)) → F

eqt(request, int(N2)) → F

eqt(request, cons(H2, T2)) → F

eqt(request, tuple(H2, T2)) → F

eqt(request, tuplenil(H2)) → F

eqt(resource, nil) → F

eqt(resource, a) → F

eqt(resource, excl) → F

eqt(resource, false) → F

eqt(resource, lock) → F

eqt(resource, locker) → F

eqt(resource, mcrlrecord) → F

eqt(resource, ok) → F

eqt(resource, pending) → F

eqt(resource, release) → F

eqt(resource, request) → F

eqt(resource, resource) → T

eqt(resource, tag) → F

eqt(resource, true) → F

eqt(resource, undefined) → F

eqt(resource, pid(N2)) → F

eqt(resource, int(N2)) → F

eqt(resource, cons(H2, T2)) → F

eqt(resource, tuple(H2, T2)) → F

eqt(resource, tuplenil(H2)) → F

eqt(tag, nil) → F

eqt(tag, a) → F

eqt(tag, excl) → F

eqt(tag, false) → F

eqt(tag, lock) → F

eqt(tag, locker) → F

eqt(tag, mcrlrecord) → F

eqt(tag, ok) → F

eqt(tag, pending) → F

eqt(tag, release) → F

eqt(tag, request) → F

eqt(tag, resource) → F

eqt(tag, tag) → T

eqt(tag, true) → F

eqt(tag, undefined) → F

eqt(tag, pid(N2)) → F

eqt(tag, int(N2)) → F

eqt(tag, cons(H2, T2)) → F

eqt(tag, tuple(H2, T2)) → F

eqt(tag, tuplenil(H2)) → F

eqt(true, nil) → F

eqt(true, a) → F

eqt(true, excl) → F

eqt(true, false) → F

eqt(true, lock) → F

eqt(true, locker) → F

eqt(true, mcrlrecord) → F

eqt(true, ok) → F

eqt(true, pending) → F

eqt(true, release) → F

eqt(true, request) → F

eqt(true, resource) → F

eqt(true, tag) → F

eqt(true, true) → T

eqt(true, undefined) → F

eqt(true, pid(N2)) → F

eqt(true, int(N2)) → F

eqt(true, cons(H2, T2)) → F

eqt(true, tuple(H2, T2)) → F

eqt(true, tuplenil(H2)) → F

eqt(undefined, nil) → F

eqt(undefined, a) → F

eqt(undefined, tuplenil(H2)) → F

eqt(pid(N1), nil) → F

eqt(pid(N1), a) → F

eqt(pid(N1), excl) → F

eqt(pid(N1), false) → F

eqt(pid(N1), lock) → F

eqt(pid(N1), locker) → F

eqt(pid(N1), mcrlrecord) → F

eqt(pid(N1), ok) → F

eqt(pid(N1), pending) → F

eqt(pid(N1), release) → F

eqt(pid(N1), request) → F

eqt(pid(N1), resource) → F

eqt(pid(N1), tag) → F

eqt(pid(N1), true) → F

eqt(pid(N1), undefined) → F

eqt(pid(N1), pid(N2)) → eqt(N1, N2)

eqt(pid(N1), int(N2)) → F

eqt(pid(N1), cons(H2, T2)) → F

eqt(pid(N1), tuple(H2, T2)) → F

eqt(pid(N1), tuplenil(H2)) → F

eqt(int(N1), nil) → F

eqt(int(N1), a) → F

eqt(int(N1), excl) → F

eqt(int(N1), false) → F

eqt(int(N1), lock) → F

eqt(int(N1), locker) → F

eqt(int(N1), mcrlrecord) → F

eqt(int(N1), ok) → F

eqt(int(N1), pending) → F

eqt(int(N1), release) → F

eqt(int(N1), request) → F

eqt(int(N1), resource) → F

eqt(int(N1), tag) → F

eqt(int(N1), true) → F

eqt(int(N1), undefined) → F

eqt(cons(H1, T1), resource) → F

eqt(cons(H1, T1), tag) → F

eqt(cons(H1, T1), true) → F

eqt(cons(H1, T1), undefined) → F

eqt(cons(H1, T1), pid(N2)) → F

eqt(cons(H1, T1), int(N2)) → F

eqt(cons(H1, T1), cons(H2, T2)) → and(eqt(H1, H2), eqt(T1, T2))

eqt(cons(H1, T1), tuple(H2, T2)) → F

eqt(cons(H1, T1), tuplenil(H2)) → F

eqt(tuple(H1, T1), nil) → F

eqt(tuple(H1, T1), a) → F

eqt(tuple(H1, T1), excl) → F

eqt(tuple(H1, T1), false) → F

eqt(tuple(H1, T1), lock) → F

eqt(tuple(H1, T1), locker) → F

eqt(tuple(H1, T1), mcrlrecord) → F

eqt(tuple(H1, T1), ok) → F

eqt(tuple(H1, T1), pending) → F

eqt(tuple(H1, T1), release) → F

eqt(tuple(H1, T1), request) → F

eqt(tuple(H1, T1), resource) → F

eqt(tuple(H1, T1), tag) → F

eqt(tuple(H1, T1), true) → F

eqt(tuple(H1, T1), undefined) → F

eqt(tuple(H1, T1), pid(N2)) → F

eqt(tuple(H1, T1), int(N2)) → F

eqt(tuple(H1, T1), cons(H2, T2)) → F

eqt(tuple(H1, T1), tuple(H2, T2)) → and(eqt(H1, H2), eqt(T1, T2))

eqt(tuple(H1, T1), tuplenil(H2)) → F

eqt(tuplenil(H1), nil) → F

eqt(tuplenil(H1), a) → F

eqt(tuplenil(H1), excl) → F

eqt(tuplenil(H1), false) → F

eqt(tuplenil(H1), lock) → F

eqt(tuplenil(H1), locker) → F

eqt(tuplenil(H1), mcrlrecord) → F

eqt(tuplenil(H1), ok) → F

eqt(tuplenil(H1), pending) → F

eqt(tuplenil(H1), release) → F

eqt(tuplenil(H1), request) → F

eqt(tuplenil(H1), resource) → F

eqt(tuplenil(H1), tag) → F

eqt(tuplenil(H1), true) → F

eqt(tuplenil(H1), undefined) → F

eqt(tuplenil(H1), pid(N2)) → F

eqt(tuplenil(H1), int(N2)) → F

eqt(tuplenil(H1), cons(H2, T2)) → F

eqt(tuplenil(H1), tuple(H2, T2)) → F

eqt(tuplenil(H1), tuplenil(H2)) → eqt(H1, H2)

element(int(s(0)), tuplenil(T1)) → T1

element(int(s(0)), tuple(T1, T2)) → T1

element(int(s(s(N1))), tuple(T1, T2)) → element(int(s(N1)), T2)

record_new(lock) → tuple(mcrlrecord, tuple(lock, tuple(undefined, tuple(nil, tuplenil(nil)))))

record_extract(tuple(mcrlrecord, tuple(lock, tuple(F0, tuple(F1, tuplenil(F2))))), lock, resource) → tuple(mcrlrecord, tuple(lock, tuple(F0, tuple(F1, tuplenil(F2)))))

record_update(tuple(mcrlrecord, tuple(lock, tuple(F0, tuple(F1, tuplenil(F2))))), lock, pending, NewF) → tuple(mcrlrecord, tuple(lock, tuple(F0, tuple(F1, tuplenil(NewF)))))

record_updates(Record, Name, nil) → Record

record_updates(Record, Name, cons(tuple(Field, tuplenil(NewF)), Fields)) → record_updates(record_update(Record, Name, Field, NewF), Name, Fields)

locker2_map_promote_pending(nil, Pending) → nil

locker2_map_promote_pending(cons(Lock, Locks), Pending) → cons(locker2_promote_pending(Lock, Pending), locker2_map_promote_pending(Locks, Pending))

locker2_map_claim_lock(nil, Resources, Client) → nil

locker2_map_claim_lock(cons(Lock, Locks), Resources, Client) → cons(locker2_claim_lock(Lock, Resources, Client), locker2_map_claim_lock(Locks, Resources, Client))

locker2_map_add_pending(nil, Resources, Client) → nil

locker2_promote_pending(Lock, Client) → case0(Client, Lock, record_extract(Lock, lock, pending))

case0(Client, Lock, cons(Client, Pendings)) → record_updates(Lock, lock, cons(tuple(excl, tuplenil(Client)), cons(tuple(pending, tuplenil(Pendings)), nil)))

case0(Client, Lock, MCRLFree0) → Lock

locker2_remove_pending(Lock, Client) → record_updates(Lock, lock, cons(tuple(pending, tuplenil(subtract(record_extract(Lock, lock, pending), cons(Client, nil)))), nil))

locker2_add_pending(Lock, Resources, Client) → case1(Client, Resources, Lock, member(record_extract(Lock, lock, resource), Resources))

case1(Client, Resources, Lock, true) → record_updates(Lock, lock, cons(tuple(pending, tuplenil(append(record_extract(Lock, lock, pending), cons(Client, nil)))), nil))

case1(Client, Resources, Lock, false) → Lock

locker2_release_lock(Lock, Client) → case2(Client, Lock, gen_modtageq(Client, record_extract(Lock, lock, excl)))

case2(Client, Lock, true) → record_updates(Lock, lock, cons(tuple(excllock, excl), nil))

case4(Client, Lock, MCRLFree1) → false

locker2_obtainables(nil, Client) → true

locker2_obtainables(cons(Lock, Locks), Client) → case5(Client, Locks, Lock, member(Client, record_extract(Lock, lock, pending)))

case5(Client, Locks, Lock, true) → andt(locker2_obtainable(Lock, Client), locker2_obtainables(Locks, Client))

case5(Client, Locks, Lock, false) → locker2_obtainables(Locks, Client)

locker2_check_available(Resource, nil) → false

locker2_check_available(Resource, cons(Lock, Locks)) → case6(Locks, Lock, Resource, equal(Resource, record_extract(Lock, lock, resource)))

case6(Locks, Lock, Resource, true) → andt(equal(record_extract(Lock, lock, excl), nil), equal(record_extract(Lock, lock, pending), nil))

case6(Locks, Lock, Resource, false) → locker2_check_available(Resource, Locks)

locker2_check_availables(nil, Locks) → true

locker2_check_availables(cons(Resource, Resources), Locks) → andt(locker2_check_available(Resource, Locks), locker2_check_availables(Resources, Locks))

locker2_adduniq(nil, List) → List

append(cons(Head, Tail), List) → cons(Head, append(Tail, List))

subtract(List, nil) → List

subtract(List, cons(Head, Tail)) → subtract(delete(Head, List), Tail)

delete(E, nil) → nil

delete(E, cons(Head, Tail)) → case8(Tail, Head, E, equal(E, Head))

case8(Tail, Head, E, true) → Tail

case8(Tail, Head, E, false) → cons(Head, delete(E, Tail))

gen_tag(Pid) → tuple(Pid, tuplenil(tag))

gen_modtageq(Client1, Client2) → equal(Client1, Client2)

member(E, nil) → false

member(E, cons(Head, Tail)) → case9(Tail, Head, E, equal(E, Head))

case9(Tail, Head, E, true) → true

case9(Tail, Head, E, false) → member(E, Tail)

eqs(empty, empty) → T

eqs(empty, stack(E2, S2)) → F

eqs(stack(E1, S1), empty) → F

eqs(stack(E1, S1), stack(E2, S2)) → and(eqt(E1, E2), eqs(S1, S2))

pushs(E1, S1) → stack(E1, S1)

pops(stack(E1, S1)) → S1

tops(stack(E1, S1)) → E1

istops(E1, empty) → F

istops(E1, stack(E2, S1)) → eqt(E1, E2)

eqc(nocalls, nocalls) → T

eqc(nocalls, calls(E2, S2, CS2)) → F

eqc(calls(E1, S1, CS1), nocalls) → F

eqc(calls(E1, S1, CS1), calls(E2, S2, CS2)) → and(eqt(E1, E2), and(eqs(S1, S2), eqc(CS1, CS2)))

push(E1, E2, nocalls) → calls(E1, stack(E2, empty), nocalls)

push(E1, E2, calls(E3, S1, CS1)) → push1(E1, E2, E3, S1, CS1, eqt(E1, E3))

push1(E1, E2, E3, S1, CS1, T) → calls(E3, pushs(E2, S1), CS1)

Rewrite Strategy: FULL




(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
eqt(pid(N1), pid(N2)) →+ eqt(N1, N2)
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [N1 / pid(N1), N2 / pid(N2)].
The result substitution is [ ].





(2) BOUNDS(n^1, INF)




(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.




(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

or(T, T) → T

or(F, T) → T

or(T, F) → T

or(F, F) → F

and(T, B) → B

and(B, T) → B

and(F, B) → F

and(B, F) → F

imp(T, B) → B

imp(F, B) → T

not(T) → F

not(F) → T

if(T, B1, B2) → B1

if(F, B1, B2) → B2

eq(T, T) → T

eq(F, F) → T

eq(T, F) → F

eq(F, T) → F

eqt(nil, undefined) → F

eqt(nil, pid(N2)) → F

eqt(nil, int(N2)) → F

eqt(nil, cons(H2, T2)) → F

eqt(nil, tuple(H2, T2)) → F

eqt(nil, tuplenil(H2)) → F

eqt(a, nil) → F

eqt(a, a) → T

eqt(a, excl) → F

eqt(a, false) → F

eqt(a, lock) → F

eqt(a, locker) → F

eqt(a, mcrlrecord) → F

eqt(a, ok) → F

eqt(a, pending) → F

eqt(a, release) → F

eqt(a, request) → F

eqt(a, resource) → F

eqt(a, tag) → F

eqt(a, true) → F

eqt(a, undefined) → F

eqt(a, pid(N2)) → F

eqt(a, int(N2)) → F

eqt(a, cons(H2, T2)) → F

eqt(a, tuple(H2, T2)) → F

eqt(a, tuplenil(H2)) → F

eqt(excl, nil) → F

eqt(excl, a) → F

eqt(excl, excl) → T

eqt(excl, false) → F

eqt(excl, lock) → F

eqt(excl, locker) → F

eqt(excl, mcrlrecord) → F

eqt(excl, ok) → F

eqt(excl, pending) → F

eqt(excl, release) → F

eqt(excl, request) → F

eqt(excl, resource) → F

eqt(excl, tag) → F

eqt(excl, true) → F

eqt(excl, undefined) → F

eqt(excl, pid(N2)) → F

eqt(excl, eqt(false, int(N2))) → F

eqt(false, cons(H2, T2)) → F

eqt(false, tuple(H2, T2)) → F

eqt(false, tuplenil(H2)) → F

eqt(lock, nil) → F

eqt(lock, a) → F

eqt(lock, excl) → F

eqt(lock, false) → F

eqt(lock, lock) → T

eqt(lock, locker) → F

eqt(lock, mcrlrecord) → F

eqt(lock, ok) → F

eqt(lock, pending) → F

eqt(lock, release) → F

eqt(lock, request) → F

eqt(lock, resource) → F

eqt(lock, tag) → F

eqt(lock, true) → F

eqt(lock, undefined) → F

eqt(lock, pid(N2)) → F

eqt(lock, int(N2)) → F

eqt(lock, cons(H2, T2)) → F

eqt(lock, tuple(H2, T2)) → F

eqt(lock, tuplenil(H2)) → F

eqt(locker, nil) → F

eqt(locker, a) → F

eqt(locker, excl) → F

eqt(locker, false) → F

eqt(locker, lock) → F

eqt(locker, locker) → T

eqt(locker, mcrlrecord) → F

eqt(locker, ok) → F

eqt(locker, pending) → F

eqt(locker, release) → F

eqt(locker, request) → F

eqt(locker, resource) → F

eqt(locker, tag) → F

eqt(locker, true) → F

eqt(locker, undefined) → F

eqt(locker, pid(N2)) → F

eqt(locker, int(N2)) → F

eqt(locker, cons(H2, T2)) → F

eqt(locker, tuple(H2, T2)) → F

eqt(locker, tuplenil(H2)) → F

eqt(mcrlrecord, nil) → F

eqt(mcrlrecord, a) → F

eqt(mcrlrecord, excl) → F

eqt(mcrlrecord, false) → F

eqt(mcrlrecord, lock) → F

eqt(mcrlrecord, locker) → F

eqt(mcrlrecord, mcrlrecord) → T

eqt(mcrlrecord, ok) → F

eqt(mcrlrecord, pending) → F

eqt(mcrlrecord, release) → F

eqt(mcrlrecord, request) → F

eqt(mcrlrecord, resource) → F

eqt(ok, resource) → F

eqt(ok, tag) → F

eqt(ok, true) → F

eqt(ok, undefined) → F

eqt(ok, pid(N2)) → F

eqt(ok, int(N2)) → F

eqt(ok, cons(H2, T2)) → F

eqt(ok, tuple(H2, T2)) → F

eqt(ok, tuplenil(H2)) → F

eqt(pending, nil) → F

eqt(pending, a) → F

eqt(pending, excl) → F

eqt(pending, false) → F

eqt(pending, lock) → F

eqt(pending, locker) → F

eqt(pending, mcrlrecord) → F

eqt(pending, ok) → F

eqt(pending, pending) → T

eqt(pending, release) → F

eqt(pending, request) → F

eqt(pending, resource) → F

eqt(pending, tag) → F

eqt(pending, true) → F

eqt(pending, undefined) → F

eqt(pending, pid(N2)) → F

eqt(pending, int(N2)) → F

eqt(pending, cons(H2, T2)) → F

eqt(pending, tuple(H2, T2)) → F

eqt(pending, tuplenil(H2)) → F

eqt(release, nil) → F

eqt(release, a) → F

eqt(release, excl) → F

eqt(release, false) → F

eqt(release, lock) → F

eqt(release, locker) → F

eqt(release, mcrlrecord) → F

eqt(release, ok) → F

eqt(request, mcrlrecord) → F

eqt(request, ok) → F

eqt(request, pending) → F

eqt(request, release) → F

eqt(request, request) → T

eqt(request, resource) → F

eqt(request, tag) → F

eqt(request, true) → F

eqt(request, undefined) → F

eqt(request, pid(N2)) → F

eqt(request, int(N2)) → F

eqt(request, cons(H2, T2)) → F

eqt(request, tuple(H2, T2)) → F

eqt(request, tuplenil(H2)) → F

eqt(resource, nil) → F

eqt(resource, a) → F

eqt(resource, excl) → F

eqt(resource, false) → F

eqt(resource, lock) → F

eqt(resource, locker) → F

eqt(resource, mcrlrecord) → F

eqt(resource, ok) → F

eqt(resource, pending) → F

eqt(resource, release) → F

eqt(resource, request) → F

eqt(resource, resource) → T

eqt(resource, tag) → F

eqt(resource, true) → F

eqt(resource, undefined) → F

eqt(resource, pid(N2)) → F

eqt(resource, int(N2)) → F

eqt(resource, cons(H2, T2)) → F

eqt(resource, tuple(H2, T2)) → F

eqt(resource, tuplenil(H2)) → F

eqt(tag, nil) → F

eqt(tag, a) → F

eqt(tag, excl) → F

eqt(tag, false) → F

eqt(tag, lock) → F

eqt(tag, locker) → F

eqt(tag, mcrlrecord) → F

eqt(tag, ok) → F

eqt(tag, pending) → F

eqt(tag, release) → F

eqt(tag, request) → F

eqt(tag, resource) → F

eqt(tag, tag) → T

eqt(tag, true) → F

eqt(tag, undefined) → F

eqt(tag, pid(N2)) → F

eqt(tag, int(N2)) → F

eqt(tag, cons(H2, T2)) → F

eqt(tag, tuple(H2, T2)) → F

eqt(tag, tuplenil(H2)) → F

eqt(true, nil) → F

eqt(true, a) → F

eqt(true, excl) → F

eqt(true, false) → F

eqt(true, lock) → F

eqt(true, locker) → F

eqt(true, mcrlrecord) → F

eqt(true, ok) → F

eqt(true, pending) → F

eqt(true, release) → F

eqt(true, request) → F

eqt(true, resource) → F

eqt(true, tag) → F

eqt(true, true) → T

eqt(true, undefined) → F

eqt(true, pid(N2)) → F

eqt(true, int(N2)) → F

eqt(true, cons(H2, T2)) → F

eqt(true, tuple(H2, T2)) → F

eqt(true, tuplenil(H2)) → F

eqt(undefined, nil) → F

eqt(undefined, a) → F

eqt(undefined, tuplenil(H2)) → F

eqt(pid(N1), nil) → F

eqt(pid(N1), a) → F

eqt(pid(N1), excl) → F

eqt(pid(N1), false) → F

eqt(pid(N1), lock) → F

eqt(pid(N1), locker) → F

eqt(pid(N1), mcrlrecord) → F

eqt(pid(N1), ok) → F

eqt(pid(N1), pending) → F

eqt(pid(N1), release) → F

eqt(pid(N1), request) → F

eqt(pid(N1), resource) → F

eqt(pid(N1), tag) → F

eqt(pid(N1), true) → F

eqt(pid(N1), undefined) → F

eqt(pid(N1), pid(N2)) → eqt(N1, N2)

eqt(pid(N1), int(N2)) → F

eqt(pid(N1), cons(H2, T2)) → F

eqt(pid(N1), tuple(H2, T2)) → F

eqt(pid(N1), tuplenil(H2)) → F

eqt(int(N1), nil) → F

eqt(int(N1), a) → F

eqt(int(N1), excl) → F

eqt(int(N1), false) → F

eqt(int(N1), lock) → F

eqt(int(N1), locker) → F

eqt(int(N1), mcrlrecord) → F

eqt(int(N1), ok) → F

eqt(int(N1), pending) → F

eqt(int(N1), release) → F

eqt(int(N1), request) → F

eqt(int(N1), resource) → F

eqt(int(N1), tag) → F

eqt(int(N1), true) → F

eqt(int(N1), undefined) → F

eqt(cons(H1, T1), resource) → F

eqt(cons(H1, T1), tag) → F

eqt(cons(H1, T1), true) → F

eqt(cons(H1, T1), undefined) → F

eqt(cons(H1, T1), pid(N2)) → F

eqt(cons(H1, T1), int(N2)) → F

eqt(cons(H1, T1), cons(H2, T2)) → and(eqt(H1, H2), eqt(T1, T2))

eqt(cons(H1, T1), tuple(H2, T2)) → F

eqt(cons(H1, T1), tuplenil(H2)) → F

eqt(tuple(H1, T1), nil) → F

eqt(tuple(H1, T1), a) → F

eqt(tuple(H1, T1), excl) → F

eqt(tuple(H1, T1), false) → F

eqt(tuple(H1, T1), lock) → F

eqt(tuple(H1, T1), locker) → F

eqt(tuple(H1, T1), mcrlrecord) → F

eqt(tuple(H1, T1), ok) → F

eqt(tuple(H1, T1), pending) → F

eqt(tuple(H1, T1), release) → F

eqt(tuple(H1, T1), request) → F

eqt(tuple(H1, T1), resource) → F

eqt(tuple(H1, T1), tag) → F

eqt(tuple(H1, T1), true) → F

eqt(tuple(H1, T1), undefined) → F

eqt(tuple(H1, T1), pid(N2)) → F

eqt(tuple(H1, T1), int(N2)) → F

eqt(tuple(H1, T1), cons(H2, T2)) → F

eqt(tuple(H1, T1), tuple(H2, T2)) → and(eqt(H1, H2), eqt(T1, T2))

eqt(tuple(H1, T1), tuplenil(H2)) → F

eqt(tuplenil(H1), nil) → F

eqt(tuplenil(H1), a) → F

eqt(tuplenil(H1), excl) → F

eqt(tuplenil(H1), false) → F

eqt(tuplenil(H1), lock) → F

eqt(tuplenil(H1), locker) → F

eqt(tuplenil(H1), mcrlrecord) → F

eqt(tuplenil(H1), ok) → F

eqt(tuplenil(H1), pending) → F

eqt(tuplenil(H1), release) → F

eqt(tuplenil(H1), request) → F

eqt(tuplenil(H1), resource) → F

eqt(tuplenil(H1), tag) → F

eqt(tuplenil(H1), true) → F

eqt(tuplenil(H1), undefined) → F

eqt(tuplenil(H1), pid(N2)) → F

eqt(tuplenil(H1), int(N2)) → F

eqt(tuplenil(H1), cons(H2, T2)) → F

eqt(tuplenil(H1), tuple(H2, T2)) → F

eqt(tuplenil(H1), tuplenil(H2)) → eqt(H1, H2)

element(int(s(0')), tuplenil(T1)) → T1

element(int(s(0')), tuple(T1, T2)) → T1

element(int(s(s(N1))), tuple(T1, T2)) → element(int(s(N1)), T2)

record_new(lock) → tuple(mcrlrecord, tuple(lock, tuple(undefined, tuple(nil, tuplenil(nil)))))

record_extract(tuple(mcrlrecord, tuple(lock, tuple(F0, tuple(F1, tuplenil(F2))))), lock, resource) → tuple(mcrlrecord, tuple(lock, tuple(F0, tuple(F1, tuplenil(F2)))))

record_update(tuple(mcrlrecord, tuple(lock, tuple(F0, tuple(F1, tuplenil(F2))))), lock, pending, NewF) → tuple(mcrlrecord, tuple(lock, tuple(F0, tuple(F1, tuplenil(NewF)))))

record_updates(Record, Name, nil) → Record

record_updates(Record, Name, cons(tuple(Field, tuplenil(NewF)), Fields)) → record_updates(record_update(Record, Name, Field, NewF), Name, Fields)

locker2_map_promote_pending(nil, Pending) → nil

locker2_map_promote_pending(cons(Lock, Locks), Pending) → cons(locker2_promote_pending(Lock, Pending), locker2_map_promote_pending(Locks, Pending))

locker2_map_claim_lock(nil, Resources, Client) → nil

locker2_map_claim_lock(cons(Lock, Locks), Resources, Client) → cons(locker2_claim_lock(Lock, Resources, Client), locker2_map_claim_lock(Locks, Resources, Client))

locker2_map_add_pending(nil, Resources, Client) → nil

locker2_promote_pending(Lock, Client) → case0(Client, Lock, record_extract(Lock, lock, pending))

case0(Client, Lock, cons(Client, Pendings)) → record_updates(Lock, lock, cons(tuple(excl, tuplenil(Client)), cons(tuple(pending, tuplenil(Pendings)), nil)))

case0(Client, Lock, MCRLFree0) → Lock

locker2_remove_pending(Lock, Client) → record_updates(Lock, lock, cons(tuple(pending, tuplenil(subtract(record_extract(Lock, lock, pending), cons(Client, nil)))), nil))

locker2_add_pending(Lock, Resources, Client) → case1(Client, Resources, Lock, member(record_extract(Lock, lock, resource), Resources))

case1(Client, Resources, Lock, true) → record_updates(Lock, lock, cons(tuple(pending, tuplenil(append(record_extract(Lock, lock, pending), cons(Client, nil)))), nil))

case1(Client, Resources, Lock, false) → Lock

locker2_release_lock(Lock, Client) → case2(Client, Lock, gen_modtageq(Client, record_extract(Lock, lock, excl)))

case2(Client, Lock, true) → record_updates(Lock, lock, cons(tuple(excllock, excl), nil))

case4(Client, Lock, MCRLFree1) → false

locker2_obtainables(nil, Client) → true

locker2_obtainables(cons(Lock, Locks), Client) → case5(Client, Locks, Lock, member(Client, record_extract(Lock, lock, pending)))

case5(Client, Locks, Lock, true) → andt(locker2_obtainable(Lock, Client), locker2_obtainables(Locks, Client))

case5(Client, Locks, Lock, false) → locker2_obtainables(Locks, Client)

locker2_check_available(Resource, nil) → false

locker2_check_available(Resource, cons(Lock, Locks)) → case6(Locks, Lock, Resource, equal(Resource, record_extract(Lock, lock, resource)))

case6(Locks, Lock, Resource, true) → andt(equal(record_extract(Lock, lock, excl), nil), equal(record_extract(Lock, lock, pending), nil))

case6(Locks, Lock, Resource, false) → locker2_check_available(Resource, Locks)

locker2_check_availables(nil, Locks) → true

locker2_check_availables(cons(Resource, Resources), Locks) → andt(locker2_check_available(Resource, Locks), locker2_check_availables(Resources, Locks))

locker2_adduniq(nil, List) → List

append(cons(Head, Tail), List) → cons(Head, append(Tail, List))

subtract(List, nil) → List

subtract(List, cons(Head, Tail)) → subtract(delete(Head, List), Tail)

delete(E, nil) → nil

delete(E, cons(Head, Tail)) → case8(Tail, Head, E, equal(E, Head))

case8(Tail, Head, E, true) → Tail

case8(Tail, Head, E, false) → cons(Head, delete(E, Tail))

gen_tag(Pid) → tuple(Pid, tuplenil(tag))

gen_modtageq(Client1, Client2) → equal(Client1, Client2)

member(E, nil) → false

member(E, cons(Head, Tail)) → case9(Tail, Head, E, equal(E, Head))

case9(Tail, Head, E, true) → true

case9(Tail, Head, E, false) → member(E, Tail)

eqs(empty, empty) → T

eqs(empty, stack(E2, S2)) → F

eqs(stack(E1, S1), empty) → F

eqs(stack(E1, S1), stack(E2, S2)) → and(eqt(E1, E2), eqs(S1, S2))

pushs(E1, S1) → stack(E1, S1)

pops(stack(E1, S1)) → S1

tops(stack(E1, S1)) → E1

istops(E1, empty) → F

istops(E1, stack(E2, S1)) → eqt(E1, E2)

eqc(nocalls, nocalls) → T

eqc(nocalls, calls(E2, S2, CS2)) → F

eqc(calls(E1, S1, CS1), nocalls) → F

eqc(calls(E1, S1, CS1), calls(E2, S2, CS2)) → and(eqt(E1, E2), and(eqs(S1, S2), eqc(CS1, CS2)))

push(E1, E2, nocalls) → calls(E1, stack(E2, empty), nocalls)

push(E1, E2, calls(E3, S1, CS1)) → push1(E1, E2, E3, S1, CS1, eqt(E1, E3))

push1(E1, E2, E3, S1, CS1, T) → calls(E3, pushs(E2, S1), CS1)

S is empty.
Rewrite Strategy: FULL




(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.




(6) Obligation:
TRS:
Rules:
or(T, T) → T
or(F, T) → T
or(T, F) → T
or(F, F) → F
and(T, B) → B
and(B, T) → B
and(F, B) → F
and(B, F) → F
imp(T, B) → B
imp(F, B) → T
not(T) → F
not(F) → T
if(T, B1, B2) → B1
if(F, B1, B2) → B2
eq(T, T) → T
eq(F, F) → T
eq(T, F) → F
eq(F, T) → F
eqt(nil, undefined) → F
eqt(nil, pid(N2)) → F
eqt(nil, int(N2)) → F
eqt(nil, cons(H2, T2)) → F
eqt(nil, tuple(H2, T2)) → F
eqt(nil, tuplenil(H2)) → F
eqt(a, nil) → F
eqt(a, a) → T
eqt(a, excl) → F
eqt(a, false) → F
eqt(a, lock) → F
eqt(a, locker) → F
eqt(a, mcrlrecord) → F
eqt(a, ok) → F
eqt(a, pending) → F
eqt(a, release) → F
eqt(a, request) → F
eqt(a, resource) → F
eqt(a, tag) → F
eqt(a, true) → F
eqt(a, undefined) → F
eqt(a, pid(N2)) → F
eqt(a, int(N2)) → F
eqt(a, cons(H2, T2)) → F
eqt(a, tuple(H2, T2)) → F
eqt(a, tuplenil(H2)) → F
eqt(excl, nil) → F
eqt(excl, a) → F
eqt(excl, excl) → T
eqt(excl, false) → F
eqt(excl, lock) → F
eqt(excl, locker) → F
eqt(excl, mcrlrecord) → F
eqt(excl, ok) → F
eqt(excl, pending) → F
eqt(excl, release) → F
eqt(excl, request) → F
eqt(excl, resource) → F
eqt(excl, tag) → F
eqt(excl, true) → F
eqt(excl, undefined) → F
eqt(excl, pid(N2)) → F
eqt(excl, eqt(false, int(N2))) → F
eqt(false, cons(H2, T2)) → F
eqt(false, tuple(H2, T2)) → F
eqt(false, tuplenil(H2)) → F
eqt(lock, nil) → F
eqt(lock, a) → F
eqt(lock, excl) → F
eqt(lock, false) → F
eqt(lock, lock) → T
eqt(lock, locker) → F
eqt(lock, mcrlrecord) → F
eqt(lock, ok) → F
eqt(lock, pending) → F
eqt(lock, release) → F
eqt(lock, request) → F
eqt(lock, resource) → F
eqt(lock, tag) → F
eqt(lock, true) → F
eqt(lock, undefined) → F
eqt(lock, pid(N2)) → F
eqt(lock, int(N2)) → F
eqt(lock, cons(H2, T2)) → F
eqt(lock, tuple(H2, T2)) → F
eqt(lock, tuplenil(H2)) → F
eqt(locker, nil) → F
eqt(locker, a) → F
eqt(locker, excl) → F
eqt(locker, false) → F
eqt(locker, lock) → F
eqt(locker, locker) → T
eqt(locker, mcrlrecord) → F
eqt(locker, ok) → F
eqt(locker, pending) → F
eqt(locker, release) → F
eqt(locker, request) → F
eqt(locker, resource) → F
eqt(locker, tag) → F
eqt(locker, true) → F
eqt(locker, undefined) → F
eqt(locker, pid(N2)) → F
eqt(locker, int(N2)) → F
eqt(locker, cons(H2, T2)) → F
eqt(locker, tuple(H2, T2)) → F
eqt(locker, tuplenil(H2)) → F
eqt(mcrlrecord, nil) → F
eqt(mcrlrecord, a) → F
eqt(mcrlrecord, excl) → F
eqt(mcrlrecord, false) → F
eqt(mcrlrecord, lock) → F
eqt(mcrlrecord, locker) → F
eqt(mcrlrecord, mcrlrecord) → T
eqt(mcrlrecord, ok) → F
eqt(mcrlrecord, pending) → F
eqt(mcrlrecord, release) → F
eqt(mcrlrecord, request) → F
eqt(mcrlrecord, resource) → F
eqt(ok, resource) → F
eqt(ok, tag) → F
eqt(ok, true) → F
eqt(ok, undefined) → F
eqt(ok, pid(N2)) → F
eqt(ok, int(N2)) → F
eqt(ok, cons(H2, T2)) → F
eqt(ok, tuple(H2, T2)) → F
eqt(ok, tuplenil(H2)) → F
eqt(pending, nil) → F
eqt(pending, a) → F
eqt(pending, excl) → F
eqt(pending, false) → F
eqt(pending, lock) → F
eqt(pending, locker) → F
eqt(pending, mcrlrecord) → F
eqt(pending, ok) → F
eqt(pending, pending) → T
eqt(pending, release) → F
eqt(pending, request) → F
eqt(pending, resource) → F
eqt(pending, tag) → F
eqt(pending, true) → F
eqt(pending, undefined) → F
eqt(pending, pid(N2)) → F
eqt(pending, int(N2)) → F
eqt(pending, cons(H2, T2)) → F
eqt(pending, tuple(H2, T2)) → F
eqt(pending, tuplenil(H2)) → F
eqt(release, nil) → F
eqt(release, a) → F
eqt(release, excl) → F
eqt(release, false) → F
eqt(release, lock) → F
eqt(release, locker) → F
eqt(release, mcrlrecord) → F
eqt(release, ok) → F
eqt(request, mcrlrecord) → F
eqt(request, ok) → F
eqt(request, pending) → F
eqt(request, release) → F
eqt(request, request) → T
eqt(request, resource) → F
eqt(request, tag) → F
eqt(request, true) → F
eqt(request, undefined) → F
eqt(request, pid(N2)) → F
eqt(request, int(N2)) → F
eqt(request, cons(H2, T2)) → F
eqt(request, tuple(H2, T2)) → F
eqt(request, tuplenil(H2)) → F
eqt(resource, nil) → F
eqt(resource, a) → F
eqt(resource, excl) → F
eqt(resource, false) → F
eqt(resource, lock) → F
eqt(resource, locker) → F
eqt(resource, mcrlrecord) → F
eqt(resource, ok) → F
eqt(resource, pending) → F
eqt(resource, release) → F
eqt(resource, request) → F
eqt(resource, resource) → T
eqt(resource, tag) → F
eqt(resource, true) → F
eqt(resource, undefined) → F
eqt(resource, pid(N2)) → F
eqt(resource, int(N2)) → F
eqt(resource, cons(H2, T2)) → F
eqt(resource, tuple(H2, T2)) → F
eqt(resource, tuplenil(H2)) → F
eqt(tag, nil) → F
eqt(tag, a) → F
eqt(tag, excl) → F
eqt(tag, false) → F
eqt(tag, lock) → F
eqt(tag, locker) → F
eqt(tag, mcrlrecord) → F
eqt(tag, ok) → F
eqt(tag, pending) → F
eqt(tag, release) → F
eqt(tag, request) → F
eqt(tag, resource) → F
eqt(tag, tag) → T
eqt(tag, true) → F
eqt(tag, undefined) → F
eqt(tag, pid(N2)) → F
eqt(tag, int(N2)) → F
eqt(tag, cons(H2, T2)) → F
eqt(tag, tuple(H2, T2)) → F
eqt(tag, tuplenil(H2)) → F
eqt(true, nil) → F
eqt(true, a) → F
eqt(true, excl) → F
eqt(true, false) → F
eqt(true, lock) → F
eqt(true, locker) → F
eqt(true, mcrlrecord) → F
eqt(true, ok) → F
eqt(true, pending) → F
eqt(true, release) → F
eqt(true, request) → F
eqt(true, resource) → F
eqt(true, tag) → F
eqt(true, true) → T
eqt(true, undefined) → F
eqt(true, pid(N2)) → F
eqt(true, int(N2)) → F
eqt(true, cons(H2, T2)) → F
eqt(true, tuple(H2, T2)) → F
eqt(true, tuplenil(H2)) → F
eqt(undefined, nil) → F
eqt(undefined, a) → F
eqt(undefined, tuplenil(H2)) → F
eqt(pid(N1), nil) → F
eqt(pid(N1), a) → F
eqt(pid(N1), excl) → F
eqt(pid(N1), false) → F
eqt(pid(N1), lock) → F
eqt(pid(N1), locker) → F
eqt(pid(N1), mcrlrecord) → F
eqt(pid(N1), ok) → F
eqt(pid(N1), pending) → F
eqt(pid(N1), release) → F
eqt(pid(N1), request) → F
eqt(pid(N1), resource) → F
eqt(pid(N1), tag) → F
eqt(pid(N1), true) → F
eqt(pid(N1), undefined) → F
eqt(pid(N1), pid(N2)) → eqt(N1, N2)
eqt(pid(N1), int(N2)) → F
eqt(pid(N1), cons(H2, T2)) → F
eqt(pid(N1), tuple(H2, T2)) → F
eqt(pid(N1), tuplenil(H2)) → F
eqt(int(N1), nil) → F
eqt(int(N1), a) → F
eqt(int(N1), excl) → F
eqt(int(N1), false) → F
eqt(int(N1), lock) → F
eqt(int(N1), locker) → F
eqt(int(N1), mcrlrecord) → F
eqt(int(N1), ok) → F
eqt(int(N1), pending) → F
eqt(int(N1), release) → F
eqt(int(N1), request) → F
eqt(int(N1), resource) → F
eqt(int(N1), tag) → F
eqt(int(N1), true) → F
eqt(int(N1), undefined) → F
eqt(cons(H1, T1), resource) → F
eqt(cons(H1, T1), tag) → F
eqt(cons(H1, T1), true) → F
eqt(cons(H1, T1), undefined) → F
eqt(cons(H1, T1), pid(N2)) → F
eqt(cons(H1, T1), int(N2)) → F
eqt(cons(H1, T1), cons(H2, T2)) → and(eqt(H1, H2), eqt(T1, T2))
eqt(cons(H1, T1), tuple(H2, T2)) → F
eqt(cons(H1, T1), tuplenil(H2)) → F
eqt(tuple(H1, T1), nil) → F
eqt(tuple(H1, T1), a) → F
eqt(tuple(H1, T1), excl) → F
eqt(tuple(H1, T1), false) → F
eqt(tuple(H1, T1), lock) → F
eqt(tuple(H1, T1), locker) → F
eqt(tuple(H1, T1), mcrlrecord) → F
eqt(tuple(H1, T1), ok) → F
eqt(tuple(H1, T1), pending) → F
eqt(tuple(H1, T1), release) → F
eqt(tuple(H1, T1), request) → F
eqt(tuple(H1, T1), resource) → F
eqt(tuple(H1, T1), tag) → F
eqt(tuple(H1, T1), true) → F
eqt(tuple(H1, T1), undefined) → F
eqt(tuple(H1, T1), pid(N2)) → F
eqt(tuple(H1, T1), int(N2)) → F
eqt(tuple(H1, T1), cons(H2, T2)) → F
eqt(tuple(H1, T1), tuple(H2, T2)) → and(eqt(H1, H2), eqt(T1, T2))
eqt(tuple(H1, T1), tuplenil(H2)) → F
eqt(tuplenil(H1), nil) → F
eqt(tuplenil(H1), a) → F
eqt(tuplenil(H1), excl) → F
eqt(tuplenil(H1), false) → F
eqt(tuplenil(H1), lock) → F
eqt(tuplenil(H1), locker) → F
eqt(tuplenil(H1), mcrlrecord) → F
eqt(tuplenil(H1), ok) → F
eqt(tuplenil(H1), pending) → F
eqt(tuplenil(H1), release) → F
eqt(tuplenil(H1), request) → F
eqt(tuplenil(H1), resource) → F
eqt(tuplenil(H1), tag) → F
eqt(tuplenil(H1), true) → F
eqt(tuplenil(H1), undefined) → F
eqt(tuplenil(H1), pid(N2)) → F
eqt(tuplenil(H1), int(N2)) → F
eqt(tuplenil(H1), cons(H2, T2)) → F
eqt(tuplenil(H1), tuple(H2, T2)) → F
eqt(tuplenil(H1), tuplenil(H2)) → eqt(H1, H2)
element(int(s(0')), tuplenil(T1)) → T1
element(int(s(0')), tuple(T1, T2)) → T1
element(int(s(s(N1))), tuple(T1, T2)) → element(int(s(N1)), T2)
record_new(lock) → tuple(mcrlrecord, tuple(lock, tuple(undefined, tuple(nil, tuplenil(nil)))))
record_extract(tuple(mcrlrecord, tuple(lock, tuple(F0, tuple(F1, tuplenil(F2))))), lock, resource) → tuple(mcrlrecord, tuple(lock, tuple(F0, tuple(F1, tuplenil(F2)))))
record_update(tuple(mcrlrecord, tuple(lock, tuple(F0, tuple(F1, tuplenil(F2))))), lock, pending, NewF) → tuple(mcrlrecord, tuple(lock, tuple(F0, tuple(F1, tuplenil(NewF)))))
record_updates(Record, Name, nil) → Record
record_updates(Record, Name, cons(tuple(Field, tuplenil(NewF)), Fields)) → record_updates(record_update(Record, Name, Field, NewF), Name, Fields)
locker2_map_promote_pending(nil, Pending) → nil
locker2_map_promote_pending(cons(Lock, Locks), Pending) → cons(locker2_promote_pending(Lock, Pending), locker2_map_promote_pending(Locks, Pending))
locker2_map_claim_lock(nil, Resources, Client) → nil
locker2_map_claim_lock(cons(Lock, Locks), Resources, Client) → cons(locker2_claim_lock(Lock, Resources, Client), locker2_map_claim_lock(Locks, Resources, Client))
locker2_map_add_pending(nil, Resources, Client) → nil
locker2_promote_pending(Lock, Client) → case0(Client, Lock, record_extract(Lock, lock, pending))
case0(Client, Lock, cons(Client, Pendings)) → record_updates(Lock, lock, cons(tuple(excl, tuplenil(Client)), cons(tuple(pending, tuplenil(Pendings)), nil)))
case0(Client, Lock, MCRLFree0) → Lock
locker2_remove_pending(Lock, Client) → record_updates(Lock, lock, cons(tuple(pending, tuplenil(subtract(record_extract(Lock, lock, pending), cons(Client, nil)))), nil))
locker2_add_pending(Lock, Resources, Client) → case1(Client, Resources, Lock, member(record_extract(Lock, lock, resource), Resources))
case1(Client, Resources, Lock, true) → record_updates(Lock, lock, cons(tuple(pending, tuplenil(append(record_extract(Lock, lock, pending), cons(Client, nil)))), nil))
case1(Client, Resources, Lock, false) → Lock
locker2_release_lock(Lock, Client) → case2(Client, Lock, gen_modtageq(Client, record_extract(Lock, lock, excl)))
case2(Client, Lock, true) → record_updates(Lock, lock, cons(tuple(excllock, excl), nil))
case4(Client, Lock, MCRLFree1) → false
locker2_obtainables(nil, Client) → true
locker2_obtainables(cons(Lock, Locks), Client) → case5(Client, Locks, Lock, member(Client, record_extract(Lock, lock, pending)))
case5(Client, Locks, Lock, true) → andt(locker2_obtainable(Lock, Client), locker2_obtainables(Locks, Client))
case5(Client, Locks, Lock, false) → locker2_obtainables(Locks, Client)
locker2_check_available(Resource, nil) → false
locker2_check_available(Resource, cons(Lock, Locks)) → case6(Locks, Lock, Resource, equal(Resource, record_extract(Lock, lock, resource)))
case6(Locks, Lock, Resource, true) → andt(equal(record_extract(Lock, lock, excl), nil), equal(record_extract(Lock, lock, pending), nil))
case6(Locks, Lock, Resource, false) → locker2_check_available(Resource, Locks)
locker2_check_availables(nil, Locks) → true
locker2_check_availables(cons(Resource, Resources), Locks) → andt(locker2_check_available(Resource, Locks), locker2_check_availables(Resources, Locks))
locker2_adduniq(nil, List) → List
append(cons(Head, Tail), List) → cons(Head, append(Tail, List))
subtract(List, nil) → List
subtract(List, cons(Head, Tail)) → subtract(delete(Head, List), Tail)
delete(E, nil) → nil
delete(E, cons(Head, Tail)) → case8(Tail, Head, E, equal(E, Head))
case8(Tail, Head, E, true) → Tail
case8(Tail, Head, E, false) → cons(Head, delete(E, Tail))
gen_tag(Pid) → tuple(Pid, tuplenil(tag))
gen_modtageq(Client1, Client2) → equal(Client1, Client2)
member(E, nil) → false
member(E, cons(Head, Tail)) → case9(Tail, Head, E, equal(E, Head))
case9(Tail, Head, E, true) → true
case9(Tail, Head, E, false) → member(E, Tail)
eqs(empty, empty) → T
eqs(empty, stack(E2, S2)) → F
eqs(stack(E1, S1), empty) → F
eqs(stack(E1, S1), stack(E2, S2)) → and(eqt(E1, E2), eqs(S1, S2))
pushs(E1, S1) → stack(E1, S1)
pops(stack(E1, S1)) → S1
tops(stack(E1, S1)) → E1
istops(E1, empty) → F
istops(E1, stack(E2, S1)) → eqt(E1, E2)
eqc(nocalls, nocalls) → T
eqc(nocalls, calls(E2, S2, CS2)) → F
eqc(calls(E1, S1, CS1), nocalls) → F
eqc(calls(E1, S1, CS1), calls(E2, S2, CS2)) → and(eqt(E1, E2), and(eqs(S1, S2), eqc(CS1, CS2)))
push(E1, E2, nocalls) → calls(E1, stack(E2, empty), nocalls)
push(E1, E2, calls(E3, S1, CS1)) → push1(E1, E2, E3, S1, CS1, eqt(E1, E3))
push1(E1, E2, E3, S1, CS1, T) → calls(E3, pushs(E2, S1), CS1)

Types:
or :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
T :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
F :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
and :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
imp :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
not :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
if :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → if → if → if
eq :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
eqt :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
nil :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
undefined :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
pid :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
int :: 0':s → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
cons :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
tuple :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
tuplenil :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
a :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
excl :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
false :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
lock :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
mcrlrecord :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
ok :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
pending :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
release :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
request :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
resource :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
tag :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
true :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
element :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
s :: 0':s → 0':s
0' :: 0':s
record_new :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
record_extract :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
record_update :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
record_updates :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_map_promote_pending :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_promote_pending :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_map_claim_lock :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → a → b → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_claim_lock :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → a → b → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_map_add_pending :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → c → d → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
case0 :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_remove_pending :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
subtract :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_add_pending :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
case1 :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
member :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
append :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_release_lock :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
case2 :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
gen_modtageq :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
excllock :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
case4 :: e → f → g → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_obtainables :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
case5 :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
andt :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_obtainable :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_check_available :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
case6 :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
equal :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_check_availables :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_adduniq :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → locker2_adduniq → locker2_adduniq
delete :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
case8 :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
gen_tag :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
case9 :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
eqs :: empty:stack → empty:stack → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
empty :: empty:stack
stack :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → empty:stack → empty:stack
pushs :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → empty:stack → empty:stack
pops :: empty:stack → empty:stack
tops :: empty:stack → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
istops :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → empty:stack → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
eqc :: nocalls:calls → nocalls:calls → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
nocalls :: nocalls:calls
calls :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → empty:stack → nocalls:calls → nocalls:calls
push :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → nocalls:calls → nocalls:calls
push1 :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → empty:stack → nocalls:calls → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → nocalls:calls
hole_T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal1_7 :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
hole_if2_7 :: if
hole_0':s3_7 :: 0':s
hole_a4_7 :: a
hole_b5_7 :: b
hole_c6_7 :: c
hole_d7_7 :: d
hole_e8_7 :: e
hole_f9_7 :: f
hole_g10_7 :: g
hole_locker2_adduniq11_7 :: locker2_adduniq
hole_empty:stack12_7 :: empty:stack
hole_nocalls:calls13_7 :: nocalls:calls
gen_T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal14_7 :: Nat → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
gen_0':s15_7 :: Nat → 0':s
gen_empty:stack16_7 :: Nat → empty:stack
gen_nocalls:calls17_7 :: Nat → nocalls:calls




(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
eqt, element, record_updates, locker2_map_promote_pending, locker2_map_claim_lock, subtract, member, append, locker2_obtainables, locker2_check_available, locker2_check_availables, delete, eqs, eqc
They will be analysed ascendingly in the following order:
eqt < eqs
eqt < eqc
delete < subtract
member < locker2_obtainables
locker2_check_available < locker2_check_availables
eqs < eqc




(8) Obligation:
TRS:
Rules:
or(T, T) → T
or(F, T) → T
or(T, F) → T
or(F, F) → F
and(T, B) → B
and(B, T) → B
and(F, B) → F
and(B, F) → F
imp(T, B) → B
imp(F, B) → T
not(T) → F
not(F) → T
if(T, B1, B2) → B1
if(F, B1, B2) → B2
eq(T, T) → T
eq(F, F) → T
eq(T, F) → F
eq(F, T) → F
eqt(nil, undefined) → F
eqt(nil, pid(N2)) → F
eqt(nil, int(N2)) → F
eqt(nil, cons(H2, T2)) → F
eqt(nil, tuple(H2, T2)) → F
eqt(nil, tuplenil(H2)) → F
eqt(a, nil) → F
eqt(a, a) → T
eqt(a, excl) → F
eqt(a, false) → F
eqt(a, lock) → F
eqt(a, locker) → F
eqt(a, mcrlrecord) → F
eqt(a, ok) → F
eqt(a, pending) → F
eqt(a, release) → F
eqt(a, request) → F
eqt(a, resource) → F
eqt(a, tag) → F
eqt(a, true) → F
eqt(a, undefined) → F
eqt(a, pid(N2)) → F
eqt(a, int(N2)) → F
eqt(a, cons(H2, T2)) → F
eqt(a, tuple(H2, T2)) → F
eqt(a, tuplenil(H2)) → F
eqt(excl, nil) → F
eqt(excl, a) → F
eqt(excl, excl) → T
eqt(excl, false) → F
eqt(excl, lock) → F
eqt(excl, locker) → F
eqt(excl, mcrlrecord) → F
eqt(excl, ok) → F
eqt(excl, pending) → F
eqt(excl, release) → F
eqt(excl, request) → F
eqt(excl, resource) → F
eqt(excl, tag) → F
eqt(excl, true) → F
eqt(excl, undefined) → F
eqt(excl, pid(N2)) → F
eqt(excl, eqt(false, int(N2))) → F
eqt(false, cons(H2, T2)) → F
eqt(false, tuple(H2, T2)) → F
eqt(false, tuplenil(H2)) → F
eqt(lock, nil) → F
eqt(lock, a) → F
eqt(lock, excl) → F
eqt(lock, false) → F
eqt(lock, lock) → T
eqt(lock, locker) → F
eqt(lock, mcrlrecord) → F
eqt(lock, ok) → F
eqt(lock, pending) → F
eqt(lock, release) → F
eqt(lock, request) → F
eqt(lock, resource) → F
eqt(lock, tag) → F
eqt(lock, true) → F
eqt(lock, undefined) → F
eqt(lock, pid(N2)) → F
eqt(lock, int(N2)) → F
eqt(lock, cons(H2, T2)) → F
eqt(lock, tuple(H2, T2)) → F
eqt(lock, tuplenil(H2)) → F
eqt(locker, nil) → F
eqt(locker, a) → F
eqt(locker, excl) → F
eqt(locker, false) → F
eqt(locker, lock) → F
eqt(locker, locker) → T
eqt(locker, mcrlrecord) → F
eqt(locker, ok) → F
eqt(locker, pending) → F
eqt(locker, release) → F
eqt(locker, request) → F
eqt(locker, resource) → F
eqt(locker, tag) → F
eqt(locker, true) → F
eqt(locker, undefined) → F
eqt(locker, pid(N2)) → F
eqt(locker, int(N2)) → F
eqt(locker, cons(H2, T2)) → F
eqt(locker, tuple(H2, T2)) → F
eqt(locker, tuplenil(H2)) → F
eqt(mcrlrecord, nil) → F
eqt(mcrlrecord, a) → F
eqt(mcrlrecord, excl) → F
eqt(mcrlrecord, false) → F
eqt(mcrlrecord, lock) → F
eqt(mcrlrecord, locker) → F
eqt(mcrlrecord, mcrlrecord) → T
eqt(mcrlrecord, ok) → F
eqt(mcrlrecord, pending) → F
eqt(mcrlrecord, release) → F
eqt(mcrlrecord, request) → F
eqt(mcrlrecord, resource) → F
eqt(ok, resource) → F
eqt(ok, tag) → F
eqt(ok, true) → F
eqt(ok, undefined) → F
eqt(ok, pid(N2)) → F
eqt(ok, int(N2)) → F
eqt(ok, cons(H2, T2)) → F
eqt(ok, tuple(H2, T2)) → F
eqt(ok, tuplenil(H2)) → F
eqt(pending, nil) → F
eqt(pending, a) → F
eqt(pending, excl) → F
eqt(pending, false) → F
eqt(pending, lock) → F
eqt(pending, locker) → F
eqt(pending, mcrlrecord) → F
eqt(pending, ok) → F
eqt(pending, pending) → T
eqt(pending, release) → F
eqt(pending, request) → F
eqt(pending, resource) → F
eqt(pending, tag) → F
eqt(pending, true) → F
eqt(pending, undefined) → F
eqt(pending, pid(N2)) → F
eqt(pending, int(N2)) → F
eqt(pending, cons(H2, T2)) → F
eqt(pending, tuple(H2, T2)) → F
eqt(pending, tuplenil(H2)) → F
eqt(release, nil) → F
eqt(release, a) → F
eqt(release, excl) → F
eqt(release, false) → F
eqt(release, lock) → F
eqt(release, locker) → F
eqt(release, mcrlrecord) → F
eqt(release, ok) → F
eqt(request, mcrlrecord) → F
eqt(request, ok) → F
eqt(request, pending) → F
eqt(request, release) → F
eqt(request, request) → T
eqt(request, resource) → F
eqt(request, tag) → F
eqt(request, true) → F
eqt(request, undefined) → F
eqt(request, pid(N2)) → F
eqt(request, int(N2)) → F
eqt(request, cons(H2, T2)) → F
eqt(request, tuple(H2, T2)) → F
eqt(request, tuplenil(H2)) → F
eqt(resource, nil) → F
eqt(resource, a) → F
eqt(resource, excl) → F
eqt(resource, false) → F
eqt(resource, lock) → F
eqt(resource, locker) → F
eqt(resource, mcrlrecord) → F
eqt(resource, ok) → F
eqt(resource, pending) → F
eqt(resource, release) → F
eqt(resource, request) → F
eqt(resource, resource) → T
eqt(resource, tag) → F
eqt(resource, true) → F
eqt(resource, undefined) → F
eqt(resource, pid(N2)) → F
eqt(resource, int(N2)) → F
eqt(resource, cons(H2, T2)) → F
eqt(resource, tuple(H2, T2)) → F
eqt(resource, tuplenil(H2)) → F
eqt(tag, nil) → F
eqt(tag, a) → F
eqt(tag, excl) → F
eqt(tag, false) → F
eqt(tag, lock) → F
eqt(tag, locker) → F
eqt(tag, mcrlrecord) → F
eqt(tag, ok) → F
eqt(tag, pending) → F
eqt(tag, release) → F
eqt(tag, request) → F
eqt(tag, resource) → F
eqt(tag, tag) → T
eqt(tag, true) → F
eqt(tag, undefined) → F
eqt(tag, pid(N2)) → F
eqt(tag, int(N2)) → F
eqt(tag, cons(H2, T2)) → F
eqt(tag, tuple(H2, T2)) → F
eqt(tag, tuplenil(H2)) → F
eqt(true, nil) → F
eqt(true, a) → F
eqt(true, excl) → F
eqt(true, false) → F
eqt(true, lock) → F
eqt(true, locker) → F
eqt(true, mcrlrecord) → F
eqt(true, ok) → F
eqt(true, pending) → F
eqt(true, release) → F
eqt(true, request) → F
eqt(true, resource) → F
eqt(true, tag) → F
eqt(true, true) → T
eqt(true, undefined) → F
eqt(true, pid(N2)) → F
eqt(true, int(N2)) → F
eqt(true, cons(H2, T2)) → F
eqt(true, tuple(H2, T2)) → F
eqt(true, tuplenil(H2)) → F
eqt(undefined, nil) → F
eqt(undefined, a) → F
eqt(undefined, tuplenil(H2)) → F
eqt(pid(N1), nil) → F
eqt(pid(N1), a) → F
eqt(pid(N1), excl) → F
eqt(pid(N1), false) → F
eqt(pid(N1), lock) → F
eqt(pid(N1), locker) → F
eqt(pid(N1), mcrlrecord) → F
eqt(pid(N1), ok) → F
eqt(pid(N1), pending) → F
eqt(pid(N1), release) → F
eqt(pid(N1), request) → F
eqt(pid(N1), resource) → F
eqt(pid(N1), tag) → F
eqt(pid(N1), true) → F
eqt(pid(N1), undefined) → F
eqt(pid(N1), pid(N2)) → eqt(N1, N2)
eqt(pid(N1), int(N2)) → F
eqt(pid(N1), cons(H2, T2)) → F
eqt(pid(N1), tuple(H2, T2)) → F
eqt(pid(N1), tuplenil(H2)) → F
eqt(int(N1), nil) → F
eqt(int(N1), a) → F
eqt(int(N1), excl) → F
eqt(int(N1), false) → F
eqt(int(N1), lock) → F
eqt(int(N1), locker) → F
eqt(int(N1), mcrlrecord) → F
eqt(int(N1), ok) → F
eqt(int(N1), pending) → F
eqt(int(N1), release) → F
eqt(int(N1), request) → F
eqt(int(N1), resource) → F
eqt(int(N1), tag) → F
eqt(int(N1), true) → F
eqt(int(N1), undefined) → F
eqt(cons(H1, T1), resource) → F
eqt(cons(H1, T1), tag) → F
eqt(cons(H1, T1), true) → F
eqt(cons(H1, T1), undefined) → F
eqt(cons(H1, T1), pid(N2)) → F
eqt(cons(H1, T1), int(N2)) → F
eqt(cons(H1, T1), cons(H2, T2)) → and(eqt(H1, H2), eqt(T1, T2))
eqt(cons(H1, T1), tuple(H2, T2)) → F
eqt(cons(H1, T1), tuplenil(H2)) → F
eqt(tuple(H1, T1), nil) → F
eqt(tuple(H1, T1), a) → F
eqt(tuple(H1, T1), excl) → F
eqt(tuple(H1, T1), false) → F
eqt(tuple(H1, T1), lock) → F
eqt(tuple(H1, T1), locker) → F
eqt(tuple(H1, T1), mcrlrecord) → F
eqt(tuple(H1, T1), ok) → F
eqt(tuple(H1, T1), pending) → F
eqt(tuple(H1, T1), release) → F
eqt(tuple(H1, T1), request) → F
eqt(tuple(H1, T1), resource) → F
eqt(tuple(H1, T1), tag) → F
eqt(tuple(H1, T1), true) → F
eqt(tuple(H1, T1), undefined) → F
eqt(tuple(H1, T1), pid(N2)) → F
eqt(tuple(H1, T1), int(N2)) → F
eqt(tuple(H1, T1), cons(H2, T2)) → F
eqt(tuple(H1, T1), tuple(H2, T2)) → and(eqt(H1, H2), eqt(T1, T2))
eqt(tuple(H1, T1), tuplenil(H2)) → F
eqt(tuplenil(H1), nil) → F
eqt(tuplenil(H1), a) → F
eqt(tuplenil(H1), excl) → F
eqt(tuplenil(H1), false) → F
eqt(tuplenil(H1), lock) → F
eqt(tuplenil(H1), locker) → F
eqt(tuplenil(H1), mcrlrecord) → F
eqt(tuplenil(H1), ok) → F
eqt(tuplenil(H1), pending) → F
eqt(tuplenil(H1), release) → F
eqt(tuplenil(H1), request) → F
eqt(tuplenil(H1), resource) → F
eqt(tuplenil(H1), tag) → F
eqt(tuplenil(H1), true) → F
eqt(tuplenil(H1), undefined) → F
eqt(tuplenil(H1), pid(N2)) → F
eqt(tuplenil(H1), int(N2)) → F
eqt(tuplenil(H1), cons(H2, T2)) → F
eqt(tuplenil(H1), tuple(H2, T2)) → F
eqt(tuplenil(H1), tuplenil(H2)) → eqt(H1, H2)
element(int(s(0')), tuplenil(T1)) → T1
element(int(s(0')), tuple(T1, T2)) → T1
element(int(s(s(N1))), tuple(T1, T2)) → element(int(s(N1)), T2)
record_new(lock) → tuple(mcrlrecord, tuple(lock, tuple(undefined, tuple(nil, tuplenil(nil)))))
record_extract(tuple(mcrlrecord, tuple(lock, tuple(F0, tuple(F1, tuplenil(F2))))), lock, resource) → tuple(mcrlrecord, tuple(lock, tuple(F0, tuple(F1, tuplenil(F2)))))
record_update(tuple(mcrlrecord, tuple(lock, tuple(F0, tuple(F1, tuplenil(F2))))), lock, pending, NewF) → tuple(mcrlrecord, tuple(lock, tuple(F0, tuple(F1, tuplenil(NewF)))))
record_updates(Record, Name, nil) → Record
record_updates(Record, Name, cons(tuple(Field, tuplenil(NewF)), Fields)) → record_updates(record_update(Record, Name, Field, NewF), Name, Fields)
locker2_map_promote_pending(nil, Pending) → nil
locker2_map_promote_pending(cons(Lock, Locks), Pending) → cons(locker2_promote_pending(Lock, Pending), locker2_map_promote_pending(Locks, Pending))
locker2_map_claim_lock(nil, Resources, Client) → nil
locker2_map_claim_lock(cons(Lock, Locks), Resources, Client) → cons(locker2_claim_lock(Lock, Resources, Client), locker2_map_claim_lock(Locks, Resources, Client))
locker2_map_add_pending(nil, Resources, Client) → nil
locker2_promote_pending(Lock, Client) → case0(Client, Lock, record_extract(Lock, lock, pending))
case0(Client, Lock, cons(Client, Pendings)) → record_updates(Lock, lock, cons(tuple(excl, tuplenil(Client)), cons(tuple(pending, tuplenil(Pendings)), nil)))
case0(Client, Lock, MCRLFree0) → Lock
locker2_remove_pending(Lock, Client) → record_updates(Lock, lock, cons(tuple(pending, tuplenil(subtract(record_extract(Lock, lock, pending), cons(Client, nil)))), nil))
locker2_add_pending(Lock, Resources, Client) → case1(Client, Resources, Lock, member(record_extract(Lock, lock, resource), Resources))
case1(Client, Resources, Lock, true) → record_updates(Lock, lock, cons(tuple(pending, tuplenil(append(record_extract(Lock, lock, pending), cons(Client, nil)))), nil))
case1(Client, Resources, Lock, false) → Lock
locker2_release_lock(Lock, Client) → case2(Client, Lock, gen_modtageq(Client, record_extract(Lock, lock, excl)))
case2(Client, Lock, true) → record_updates(Lock, lock, cons(tuple(excllock, excl), nil))
case4(Client, Lock, MCRLFree1) → false
locker2_obtainables(nil, Client) → true
locker2_obtainables(cons(Lock, Locks), Client) → case5(Client, Locks, Lock, member(Client, record_extract(Lock, lock, pending)))
case5(Client, Locks, Lock, true) → andt(locker2_obtainable(Lock, Client), locker2_obtainables(Locks, Client))
case5(Client, Locks, Lock, false) → locker2_obtainables(Locks, Client)
locker2_check_available(Resource, nil) → false
locker2_check_available(Resource, cons(Lock, Locks)) → case6(Locks, Lock, Resource, equal(Resource, record_extract(Lock, lock, resource)))
case6(Locks, Lock, Resource, true) → andt(equal(record_extract(Lock, lock, excl), nil), equal(record_extract(Lock, lock, pending), nil))
case6(Locks, Lock, Resource, false) → locker2_check_available(Resource, Locks)
locker2_check_availables(nil, Locks) → true
locker2_check_availables(cons(Resource, Resources), Locks) → andt(locker2_check_available(Resource, Locks), locker2_check_availables(Resources, Locks))
locker2_adduniq(nil, List) → List
append(cons(Head, Tail), List) → cons(Head, append(Tail, List))
subtract(List, nil) → List
subtract(List, cons(Head, Tail)) → subtract(delete(Head, List), Tail)
delete(E, nil) → nil
delete(E, cons(Head, Tail)) → case8(Tail, Head, E, equal(E, Head))
case8(Tail, Head, E, true) → Tail
case8(Tail, Head, E, false) → cons(Head, delete(E, Tail))
gen_tag(Pid) → tuple(Pid, tuplenil(tag))
gen_modtageq(Client1, Client2) → equal(Client1, Client2)
member(E, nil) → false
member(E, cons(Head, Tail)) → case9(Tail, Head, E, equal(E, Head))
case9(Tail, Head, E, true) → true
case9(Tail, Head, E, false) → member(E, Tail)
eqs(empty, empty) → T
eqs(empty, stack(E2, S2)) → F
eqs(stack(E1, S1), empty) → F
eqs(stack(E1, S1), stack(E2, S2)) → and(eqt(E1, E2), eqs(S1, S2))
pushs(E1, S1) → stack(E1, S1)
pops(stack(E1, S1)) → S1
tops(stack(E1, S1)) → E1
istops(E1, empty) → F
istops(E1, stack(E2, S1)) → eqt(E1, E2)
eqc(nocalls, nocalls) → T
eqc(nocalls, calls(E2, S2, CS2)) → F
eqc(calls(E1, S1, CS1), nocalls) → F
eqc(calls(E1, S1, CS1), calls(E2, S2, CS2)) → and(eqt(E1, E2), and(eqs(S1, S2), eqc(CS1, CS2)))
push(E1, E2, nocalls) → calls(E1, stack(E2, empty), nocalls)
push(E1, E2, calls(E3, S1, CS1)) → push1(E1, E2, E3, S1, CS1, eqt(E1, E3))
push1(E1, E2, E3, S1, CS1, T) → calls(E3, pushs(E2, S1), CS1)

Types:
or :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
T :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
F :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
and :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
imp :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
not :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
if :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → if → if → if
eq :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
eqt :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
nil :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
undefined :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
pid :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
int :: 0':s → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
cons :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
tuple :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
tuplenil :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
a :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
excl :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
false :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
lock :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
mcrlrecord :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
ok :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
pending :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
release :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
request :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
resource :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
tag :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
true :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
element :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
s :: 0':s → 0':s
0' :: 0':s
record_new :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
record_extract :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
record_update :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
record_updates :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_map_promote_pending :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_promote_pending :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_map_claim_lock :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → a → b → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_claim_lock :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → a → b → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_map_add_pending :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → c → d → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
case0 :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_remove_pending :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
subtract :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_add_pending :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
case1 :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
member :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
append :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_release_lock :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
case2 :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
gen_modtageq :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
excllock :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
case4 :: e → f → g → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_obtainables :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
case5 :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
andt :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_obtainable :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_check_available :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
case6 :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
equal :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_check_availables :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
locker2_adduniq :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → locker2_adduniq → locker2_adduniq
delete :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
case8 :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
gen_tag :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
case9 :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
eqs :: empty:stack → empty:stack → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
empty :: empty:stack
stack :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → empty:stack → empty:stack
pushs :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → empty:stack → empty:stack
pops :: empty:stack → empty:stack
tops :: empty:stack → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
istops :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → empty:stack → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
eqc :: nocalls:calls → nocalls:calls → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
nocalls :: nocalls:calls
calls :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → empty:stack → nocalls:calls → nocalls:calls
push :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → nocalls:calls → nocalls:calls
push1 :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → empty:stack → nocalls:calls → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal → nocalls:calls
hole_T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal1_7 :: T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
hole_if2_7 :: if
hole_0':s3_7 :: 0':s
hole_a4_7 :: a
hole_b5_7 :: b
hole_c6_7 :: c
hole_d7_7 :: d
hole_e8_7 :: e
hole_f9_7 :: f
hole_g10_7 :: g
hole_locker2_adduniq11_7 :: locker2_adduniq
hole_empty:stack12_7 :: empty:stack
hole_nocalls:calls13_7 :: nocalls:calls
gen_T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal14_7 :: Nat → T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal
gen_0':s15_7 :: Nat → 0':s
gen_empty:stack16_7 :: Nat → empty:stack
gen_nocalls:calls17_7 :: Nat → nocalls:calls
Generator Equations:
gen_T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal14_7(0) ⇔ T
gen_T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal14_7(+(x, 1)) ⇔ pid(gen_T:F:nil:undefined:pid:int:cons:tuple:tuplenil:a:excl:false:lock:locker:mcrlrecord:ok:pending:release:request:resource:tag:true:locker2_claim_lock:excllock:locker2_obtainable:andt:equal14_7(x))
gen_0':s15_7(0) ⇔ 0'
gen_0':s15_7(+(x, 1)) ⇔ s(gen_0':s15_7(x))
gen_empty:stack16_7(0) ⇔ empty
gen_empty:stack16_7(+(x, 1)) ⇔ stack(T, gen_empty:stack16_7(x))
gen_nocalls:calls17_7(0) ⇔ nocalls
gen_nocalls:calls17_7(+(x, 1)) ⇔ calls(T, empty, gen_nocalls:calls17_7(x))
The following defined symbols remain to be analysed:
eqt, element, record_updates, locker2_map_promote_pending, locker2_map_claim_lock, subtract, member, append, locker2_obtainables, locker2_check_available, locker2_check_availables, delete, eqs, eqc
They will be analysed ascendingly in the following order:
eqt < eqs
eqt < eqc
delete < subtract
member < locker2_obtainables
locker2_check_available < locker2_check_availables
eqs < eqc